Nuprl Lemma : concat_append
11,40
postcript
pdf
ll1
,
ll2
:(top List List). sqequal(concat(append(
ll1
;
ll2
)); append(concat(
ll1
); concat(
ll2
)))
latex
Definitions
x
:
A
.
B
(
x
)
,
concat(
ll
)
,
append(
as
;
bs
)
,
reduce(
f
;
k
;
as
)
,
Y
,
t
T
Lemmas
top
wf
,
append
assoc
sq
,
concat
wf
origin
ll1,ll2:(top List List). sqequal(concat(append(ll1; ll2)); append(concat(ll1); concat(ll2))) ll1,ll2:(top List List). sqequal(concat(append(ll1; ll2)); append(concat(ll1); concat(ll2))) x:A. B(x)
T